0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 14 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 2154 ms)
↳10 BOUNDS(1, n^2)
ge(0, 0) → true
ge(s(x), 0) → ge(x, 0)
ge(0, s(0)) → false
ge(0, s(s(x))) → ge(0, s(x))
ge(s(x), s(y)) → ge(x, y)
minus(0, 0) → 0
minus(0, s(x)) → minus(0, x)
minus(s(x), 0) → s(minus(x, 0))
minus(s(x), s(y)) → minus(x, y)
plus(0, 0) → 0
plus(0, s(x)) → s(plus(0, x))
plus(s(x), y) → s(plus(x, y))
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))
ge(0, 0) → true [1]
ge(s(x), 0) → ge(x, 0) [1]
ge(0, s(0)) → false [1]
ge(0, s(s(x))) → ge(0, s(x)) [1]
ge(s(x), s(y)) → ge(x, y) [1]
minus(0, 0) → 0 [1]
minus(0, s(x)) → minus(0, x) [1]
minus(s(x), 0) → s(minus(x, 0)) [1]
minus(s(x), s(y)) → minus(x, y) [1]
plus(0, 0) → 0 [1]
plus(0, s(x)) → s(plus(0, x)) [1]
plus(s(x), y) → s(plus(x, y)) [1]
div(x, y) → ify(ge(y, s(0)), x, y) [1]
ify(false, x, y) → divByZeroError [1]
ify(true, x, y) → if(ge(x, y), x, y) [1]
if(false, x, y) → 0 [1]
if(true, x, y) → s(div(minus(x, y), y)) [1]
ge(0, 0) → true [1]
ge(s(x), 0) → ge(x, 0) [1]
ge(0, s(0)) → false [1]
ge(0, s(s(x))) → ge(0, s(x)) [1]
ge(s(x), s(y)) → ge(x, y) [1]
minus(0, 0) → 0 [1]
minus(0, s(x)) → minus(0, x) [1]
minus(s(x), 0) → s(minus(x, 0)) [1]
minus(s(x), s(y)) → minus(x, y) [1]
plus(0, 0) → 0 [1]
plus(0, s(x)) → s(plus(0, x)) [1]
plus(s(x), y) → s(plus(x, y)) [1]
div(x, y) → ify(ge(y, s(0)), x, y) [1]
ify(false, x, y) → divByZeroError [1]
ify(true, x, y) → if(ge(x, y), x, y) [1]
if(false, x, y) → 0 [1]
if(true, x, y) → s(div(minus(x, y), y)) [1]
| ge :: 0:s:divByZeroError → 0:s:divByZeroError → true:false 0 :: 0:s:divByZeroError true :: true:false s :: 0:s:divByZeroError → 0:s:divByZeroError false :: true:false minus :: 0:s:divByZeroError → 0:s:divByZeroError → 0:s:divByZeroError plus :: 0:s:divByZeroError → 0:s:divByZeroError → 0:s:divByZeroError div :: 0:s:divByZeroError → 0:s:divByZeroError → 0:s:divByZeroError ify :: true:false → 0:s:divByZeroError → 0:s:divByZeroError → 0:s:divByZeroError divByZeroError :: 0:s:divByZeroError if :: true:false → 0:s:divByZeroError → 0:s:divByZeroError → 0:s:divByZeroError |
ge(v0, v1) → null_ge [0]
minus(v0, v1) → null_minus [0]
plus(v0, v1) → null_plus [0]
ify(v0, v1, v2) → null_ify [0]
if(v0, v1, v2) → null_if [0]
null_ge, null_minus, null_plus, null_ify, null_if
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
true => 2
false => 1
divByZeroError => 1
null_ge => 0
null_minus => 0
null_plus => 0
null_ify => 0
null_if => 0
div(z, z') -{ 1 }→ ify(ge(y, 1 + 0), x, y) :|: x >= 0, y >= 0, z = x, z' = y
ge(z, z') -{ 1 }→ ge(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
ge(z, z') -{ 1 }→ ge(x, 0) :|: x >= 0, z = 1 + x, z' = 0
ge(z, z') -{ 1 }→ ge(0, 1 + x) :|: x >= 0, z = 0, z' = 1 + (1 + x)
ge(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
ge(z, z') -{ 1 }→ 1 :|: z' = 1 + 0, z = 0
ge(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
if(z, z', z'') -{ 1 }→ 0 :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
if(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
if(z, z', z'') -{ 1 }→ 1 + div(minus(x, y), y) :|: z = 2, z' = x, z'' = y, x >= 0, y >= 0
ify(z, z', z'') -{ 1 }→ if(ge(x, y), x, y) :|: z = 2, z' = x, z'' = y, x >= 0, y >= 0
ify(z, z', z'') -{ 1 }→ 1 :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
ify(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
minus(z, z') -{ 1 }→ minus(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
minus(z, z') -{ 1 }→ minus(0, x) :|: z' = 1 + x, x >= 0, z = 0
minus(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
minus(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
minus(z, z') -{ 1 }→ 1 + minus(x, 0) :|: x >= 0, z = 1 + x, z' = 0
plus(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
plus(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
plus(z, z') -{ 1 }→ 1 + plus(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
plus(z, z') -{ 1 }→ 1 + plus(0, x) :|: z' = 1 + x, x >= 0, z = 0
| eq(start(V, V1, V15),0,[ge(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V15),0,[minus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V15),0,[plus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V15),0,[div(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V15),0,[ify(V, V1, V15, Out)],[V >= 0,V1 >= 0,V15 >= 0]). eq(start(V, V1, V15),0,[if(V, V1, V15, Out)],[V >= 0,V1 >= 0,V15 >= 0]). eq(ge(V, V1, Out),1,[],[Out = 2,V = 0,V1 = 0]). eq(ge(V, V1, Out),1,[ge(V2, 0, Ret)],[Out = Ret,V2 >= 0,V = 1 + V2,V1 = 0]). eq(ge(V, V1, Out),1,[],[Out = 1,V1 = 1,V = 0]). eq(ge(V, V1, Out),1,[ge(0, 1 + V3, Ret1)],[Out = Ret1,V3 >= 0,V = 0,V1 = 2 + V3]). eq(ge(V, V1, Out),1,[ge(V4, V5, Ret2)],[Out = Ret2,V1 = 1 + V5,V4 >= 0,V5 >= 0,V = 1 + V4]). eq(minus(V, V1, Out),1,[],[Out = 0,V = 0,V1 = 0]). eq(minus(V, V1, Out),1,[minus(0, V6, Ret3)],[Out = Ret3,V1 = 1 + V6,V6 >= 0,V = 0]). eq(minus(V, V1, Out),1,[minus(V7, 0, Ret11)],[Out = 1 + Ret11,V7 >= 0,V = 1 + V7,V1 = 0]). eq(minus(V, V1, Out),1,[minus(V8, V9, Ret4)],[Out = Ret4,V1 = 1 + V9,V8 >= 0,V9 >= 0,V = 1 + V8]). eq(plus(V, V1, Out),1,[],[Out = 0,V = 0,V1 = 0]). eq(plus(V, V1, Out),1,[plus(0, V10, Ret12)],[Out = 1 + Ret12,V1 = 1 + V10,V10 >= 0,V = 0]). eq(plus(V, V1, Out),1,[plus(V11, V12, Ret13)],[Out = 1 + Ret13,V11 >= 0,V12 >= 0,V = 1 + V11,V1 = V12]). eq(div(V, V1, Out),1,[ge(V13, 1 + 0, Ret0),ify(Ret0, V14, V13, Ret5)],[Out = Ret5,V14 >= 0,V13 >= 0,V = V14,V1 = V13]). eq(ify(V, V1, V15, Out),1,[],[Out = 1,V1 = V16,V15 = V17,V = 1,V16 >= 0,V17 >= 0]). eq(ify(V, V1, V15, Out),1,[ge(V18, V19, Ret01),if(Ret01, V18, V19, Ret6)],[Out = Ret6,V = 2,V1 = V18,V15 = V19,V18 >= 0,V19 >= 0]). eq(if(V, V1, V15, Out),1,[],[Out = 0,V1 = V20,V15 = V21,V = 1,V20 >= 0,V21 >= 0]). eq(if(V, V1, V15, Out),1,[minus(V22, V23, Ret10),div(Ret10, V23, Ret14)],[Out = 1 + Ret14,V = 2,V1 = V22,V15 = V23,V22 >= 0,V23 >= 0]). eq(ge(V, V1, Out),0,[],[Out = 0,V24 >= 0,V25 >= 0,V = V24,V1 = V25]). eq(minus(V, V1, Out),0,[],[Out = 0,V26 >= 0,V27 >= 0,V = V26,V1 = V27]). eq(plus(V, V1, Out),0,[],[Out = 0,V28 >= 0,V29 >= 0,V = V28,V1 = V29]). eq(ify(V, V1, V15, Out),0,[],[Out = 0,V30 >= 0,V15 = V31,V32 >= 0,V = V30,V1 = V32,V31 >= 0]). eq(if(V, V1, V15, Out),0,[],[Out = 0,V33 >= 0,V15 = V34,V35 >= 0,V = V33,V1 = V35,V34 >= 0]). input_output_vars(ge(V,V1,Out),[V,V1],[Out]). input_output_vars(minus(V,V1,Out),[V,V1],[Out]). input_output_vars(plus(V,V1,Out),[V,V1],[Out]). input_output_vars(div(V,V1,Out),[V,V1],[Out]). input_output_vars(ify(V,V1,V15,Out),[V,V1,V15],[Out]). input_output_vars(if(V,V1,V15,Out),[V,V1,V15],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [ge/3]
1. recursive : [minus/3]
2. recursive : [ (div)/3,if/4,ify/4]
3. recursive : [plus/3]
4. non_recursive : [start/3]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into ge/3
1. SCC is partially evaluated into minus/3
2. SCC is partially evaluated into (div)/3
3. SCC is partially evaluated into plus/3
4. SCC is partially evaluated into start/3
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations ge/3
* CE 17 is refined into CE [32]
* CE 14 is refined into CE [33]
* CE 12 is refined into CE [34]
* CE 16 is refined into CE [35]
* CE 13 is refined into CE [36]
* CE 15 is refined into CE [37]
### Cost equations --> "Loop" of ge/3
* CEs [35] --> Loop 19
* CEs [36] --> Loop 20
* CEs [37] --> Loop 21
* CEs [32] --> Loop 22
* CEs [33] --> Loop 23
* CEs [34] --> Loop 24
### Ranking functions of CR ge(V,V1,Out)
* RF of phase [19]: [V,V1]
* RF of phase [20]: [V]
* RF of phase [21]: [V1-1]
#### Partial ranking functions of CR ge(V,V1,Out)
* Partial RF of phase [19]:
- RF of loop [19:1]:
V
V1
* Partial RF of phase [20]:
- RF of loop [20:1]:
V
* Partial RF of phase [21]:
- RF of loop [21:1]:
V1-1
### Specialization of cost equations minus/3
* CE 18 is refined into CE [38]
* CE 22 is refined into CE [39]
* CE 21 is refined into CE [40]
* CE 20 is refined into CE [41]
* CE 19 is refined into CE [42]
### Cost equations --> "Loop" of minus/3
* CEs [40] --> Loop 25
* CEs [41] --> Loop 26
* CEs [42] --> Loop 27
* CEs [38,39] --> Loop 28
### Ranking functions of CR minus(V,V1,Out)
* RF of phase [25]: [V,V1]
* RF of phase [26]: [V]
* RF of phase [27]: [V1]
#### Partial ranking functions of CR minus(V,V1,Out)
* Partial RF of phase [25]:
- RF of loop [25:1]:
V
V1
* Partial RF of phase [26]:
- RF of loop [26:1]:
V
* Partial RF of phase [27]:
- RF of loop [27:1]:
V1
### Specialization of cost equations (div)/3
* CE 24 is refined into CE [43]
* CE 23 is refined into CE [44,45,46,47]
* CE 25 is refined into CE [48,49,50,51]
* CE 27 is refined into CE [52,53,54,55,56,57,58,59,60,61]
* CE 26 is refined into CE [62,63,64,65,66,67]
### Cost equations --> "Loop" of (div)/3
* CEs [67] --> Loop 29
* CEs [66] --> Loop 30
* CEs [65] --> Loop 31
* CEs [64] --> Loop 32
* CEs [63] --> Loop 33
* CEs [62] --> Loop 34
* CEs [60] --> Loop 35
* CEs [50,58] --> Loop 36
* CEs [43] --> Loop 37
* CEs [44] --> Loop 38
* CEs [54] --> Loop 39
* CEs [49,57] --> Loop 40
* CEs [45,46,47,48,51,52,53,55,56,59,61] --> Loop 41
### Ranking functions of CR div(V,V1,Out)
* RF of phase [29]: [V/2-1,V/2-V1/2]
* RF of phase [32]: [V-1]
#### Partial ranking functions of CR div(V,V1,Out)
* Partial RF of phase [29]:
- RF of loop [29:1]:
V/2-1
V/2-V1/2
* Partial RF of phase [32]:
- RF of loop [32:1]:
V-1
### Specialization of cost equations plus/3
* CE 28 is refined into CE [68]
* CE 31 is refined into CE [69]
* CE 30 is refined into CE [70]
* CE 29 is refined into CE [71]
### Cost equations --> "Loop" of plus/3
* CEs [70] --> Loop 42
* CEs [71] --> Loop 43
* CEs [68,69] --> Loop 44
### Ranking functions of CR plus(V,V1,Out)
* RF of phase [42]: [V]
* RF of phase [43]: [V1]
#### Partial ranking functions of CR plus(V,V1,Out)
* Partial RF of phase [42]:
- RF of loop [42:1]:
V
* Partial RF of phase [43]:
- RF of loop [43:1]:
V1
### Specialization of cost equations start/3
* CE 4 is refined into CE [72,73,74,75]
* CE 5 is refined into CE [76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97]
* CE 6 is refined into CE [98,99,100,101,102,103,104,105,106,107]
* CE 7 is refined into CE [108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124]
* CE 2 is refined into CE [125]
* CE 3 is refined into CE [126]
* CE 8 is refined into CE [127,128,129,130,131,132,133,134,135,136]
* CE 9 is refined into CE [137,138,139]
* CE 10 is refined into CE [140,141,142,143]
* CE 11 is refined into CE [144,145,146,147,148,149,150,151,152,153,154,155,156]
### Cost equations --> "Loop" of start/3
* CEs [133,152] --> Loop 45
* CEs [149,150] --> Loop 46
* CEs [85,106] --> Loop 47
* CEs [74,104] --> Loop 48
* CEs [88,89,90,91,115,116,117,118] --> Loop 49
* CEs [73,101] --> Loop 50
* CEs [72,99] --> Loop 51
* CEs [75,76,77,78,79,80,81,82,83,84,86,87,92,93,94,95,96,97,98,100,102,103,105,107,108,109,110,111,112,113,114,119,120,121,122,123,124] --> Loop 52
* CEs [126] --> Loop 53
* CEs [135,145,146,151,153] --> Loop 54
* CEs [128,130,140] --> Loop 55
* CEs [125,127,129,131,132,134,136,137,138,139,141,142,143,144,147,148,154,155,156] --> Loop 56
### Ranking functions of CR start(V,V1,V15)
#### Partial ranking functions of CR start(V,V1,V15)
Computing Bounds
=====================================
#### Cost of chains of ge(V,V1,Out):
* Chain [[21],23]: 1*it(21)+1
Such that:it(21) =< V1
with precondition: [V=0,Out=1,V1>=2]
* Chain [[21],22]: 1*it(21)+0
Such that:it(21) =< V1
with precondition: [V=0,Out=0,V1>=2]
* Chain [[20],24]: 1*it(20)+1
Such that:it(20) =< V
with precondition: [V1=0,Out=2,V>=1]
* Chain [[20],22]: 1*it(20)+0
Such that:it(20) =< V
with precondition: [V1=0,Out=0,V>=1]
* Chain [[19],[21],23]: 1*it(19)+1*it(21)+1
Such that:it(21) =< -V+V1
it(19) =< V
with precondition: [Out=1,V>=1,V1>=V+2]
* Chain [[19],[21],22]: 1*it(19)+1*it(21)+0
Such that:it(21) =< -V+V1
it(19) =< V
with precondition: [Out=0,V>=1,V1>=V+2]
* Chain [[19],[20],24]: 1*it(19)+1*it(20)+1
Such that:it(20) =< V-V1
it(19) =< V1
with precondition: [Out=2,V1>=1,V>=V1+1]
* Chain [[19],[20],22]: 1*it(19)+1*it(20)+0
Such that:it(20) =< V-V1
it(19) =< V1
with precondition: [Out=0,V1>=1,V>=V1+1]
* Chain [[19],24]: 1*it(19)+1
Such that:it(19) =< V
with precondition: [Out=2,V=V1,V>=1]
* Chain [[19],23]: 1*it(19)+1
Such that:it(19) =< V
with precondition: [Out=1,V+1=V1,V>=1]
* Chain [[19],22]: 1*it(19)+0
Such that:it(19) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [24]: 1
with precondition: [V=0,V1=0,Out=2]
* Chain [23]: 1
with precondition: [V=0,V1=1,Out=1]
* Chain [22]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of minus(V,V1,Out):
* Chain [[27],28]: 1*it(27)+1
Such that:it(27) =< V1
with precondition: [V=0,Out=0,V1>=1]
* Chain [[26],28]: 1*it(26)+1
Such that:it(26) =< Out
with precondition: [V1=0,Out>=1,V>=Out]
* Chain [[25],[27],28]: 1*it(25)+1*it(27)+1
Such that:it(27) =< -V+V1
it(25) =< V
with precondition: [Out=0,V>=1,V1>=V+1]
* Chain [[25],[26],28]: 1*it(25)+1*it(26)+1
Such that:it(25) =< V1
it(26) =< Out
with precondition: [V1>=1,Out>=1,V>=Out+V1]
* Chain [[25],28]: 1*it(25)+1
Such that:it(25) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [28]: 1
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of div(V,V1,Out):
* Chain [[32],41]: 17*it(32)+28*s(12)+1*s(59)+1*s(60)+5
Such that:aux(21) =< 1
aux(22) =< V
s(12) =< aux(21)
it(32) =< aux(22)
aux(17) =< aux(22)-1
s(59) =< it(32)*aux(22)
s(60) =< it(32)*aux(17)
with precondition: [V1=1,Out>=1,V>=Out+1]
* Chain [[32],39]: 9*it(32)+1*s(59)+1*s(60)+2*s(62)+4
Such that:aux(23) =< 1
aux(24) =< V
s(62) =< aux(23)
it(32) =< aux(24)
aux(17) =< aux(24)-1
s(59) =< it(32)*aux(24)
s(60) =< it(32)*aux(17)
with precondition: [V1=1,Out>=1,V>=Out+1]
* Chain [[32],34,41]: 9*it(32)+37*s(12)+1*s(59)+1*s(60)+11
Such that:aux(27) =< 1
aux(28) =< V
s(12) =< aux(27)
it(32) =< aux(28)
aux(17) =< aux(28)-1
s(59) =< it(32)*aux(28)
s(60) =< it(32)*aux(17)
with precondition: [V1=1,Out>=2,V>=Out]
* Chain [[32],33,41]: 11*it(32)+36*s(12)+1*s(59)+1*s(60)+11
Such that:aux(32) =< 1
aux(33) =< V
s(12) =< aux(32)
it(32) =< aux(33)
aux(17) =< aux(33)-1
s(59) =< it(32)*aux(33)
s(60) =< it(32)*aux(17)
with precondition: [V1=1,Out>=2,V>=Out+1]
* Chain [[29],41]: 6*it(29)+1*s(11)+14*s(12)+17*s(15)+9*s(23)+2*s(38)+1*s(89)+1*s(90)+1*s(91)+5
Such that:aux(9) =< 1
aux(12) =< V-2*V1-2*Out+2
aux(36) =< V-V1
aux(38) =< V/2
aux(39) =< V/2-V1/2
s(11) =< -V1+1
aux(42) =< V
aux(43) =< V1
s(15) =< aux(9)
s(12) =< aux(43)
s(23) =< aux(42)
s(38) =< aux(12)
aux(35) =< aux(38)
it(29) =< aux(38)
aux(35) =< aux(39)
it(29) =< aux(39)
aux(35) =< aux(42)
it(29) =< aux(42)
aux(37) =< aux(36)
s(90) =< it(29)*aux(36)
s(89) =< aux(35)
s(91) =< it(29)*aux(37)
with precondition: [V1>=2,Out>=1,V+1>=2*Out+V1]
* Chain [[29],36]: 6*it(29)+3*s(88)+1*s(89)+1*s(90)+1*s(91)+4*s(93)+2*s(94)+5
Such that:aux(46) =< 1
aux(36) =< V-V1
s(92) =< V-V1+1
aux(38) =< V/2
aux(39) =< V/2-V1/2
aux(47) =< V1
aux(48) =< V/2-V1/2+1/2
s(94) =< aux(46)
s(93) =< aux(47)
aux(35) =< aux(38)
it(29) =< aux(38)
aux(35) =< aux(39)
it(29) =< aux(39)
aux(35) =< aux(48)
it(29) =< aux(48)
aux(37) =< aux(36)
s(90) =< it(29)*aux(36)
s(89) =< aux(35)
s(91) =< it(29)*aux(37)
s(88) =< s(92)
with precondition: [V1>=2,Out>=1,V+3>=2*Out+2*V1]
* Chain [[29],35]: 6*it(29)+3*s(88)+1*s(89)+1*s(90)+1*s(91)+2*s(99)+1*s(100)+4
Such that:s(100) =< 1
aux(38) =< V/2
aux(49) =< V1
aux(50) =< V-V1
aux(51) =< V/2-V1/2
s(99) =< aux(49)
aux(35) =< aux(38)
it(29) =< aux(38)
aux(35) =< aux(51)
it(29) =< aux(51)
aux(37) =< aux(50)
s(90) =< it(29)*aux(50)
s(89) =< aux(35)
s(91) =< it(29)*aux(37)
s(88) =< aux(50)
with precondition: [V1>=2,Out>=1,V+2>=2*Out+2*V1]
* Chain [[29],31,41]: 6*it(29)+1*s(11)+19*s(12)+19*s(15)+2*s(38)+3*s(88)+1*s(89)+1*s(90)+1*s(91)+11
Such that:aux(53) =< 1
aux(38) =< V/2
aux(12) =< -V1
s(11) =< -V1+1
aux(54) =< V1
aux(55) =< V-V1
aux(56) =< V/2-V1/2
s(15) =< aux(53)
s(12) =< aux(54)
s(38) =< aux(12)
aux(35) =< aux(38)
it(29) =< aux(38)
aux(35) =< aux(56)
it(29) =< aux(56)
aux(37) =< aux(55)
s(90) =< it(29)*aux(55)
s(89) =< aux(35)
s(91) =< it(29)*aux(37)
s(88) =< aux(55)
with precondition: [V1>=2,Out>=2,V+4>=2*Out+2*V1]
* Chain [[29],31,40]: 6*it(29)+3*s(88)+1*s(89)+1*s(90)+1*s(91)+9*s(102)+3*s(103)+11
Such that:aux(61) =< 1
aux(38) =< V/2
aux(62) =< V1
aux(63) =< V-V1
aux(64) =< V/2-V1/2
s(103) =< aux(61)
s(102) =< aux(62)
aux(35) =< aux(38)
it(29) =< aux(38)
aux(35) =< aux(64)
it(29) =< aux(64)
aux(37) =< aux(63)
s(90) =< it(29)*aux(63)
s(89) =< aux(35)
s(91) =< it(29)*aux(37)
s(88) =< aux(63)
with precondition: [V1>=2,Out>=2,V+4>=2*Out+2*V1]
* Chain [[29],30,41]: 6*it(29)+1*s(11)+18*s(12)+19*s(15)+2*s(38)+4*s(88)+1*s(89)+1*s(90)+1*s(91)+1*s(117)+11
Such that:aux(66) =< 1
aux(38) =< V/2
aux(39) =< V/2-V1/2
aux(12) =< -V1
s(11) =< -V1+1
aux(67) =< V1
aux(68) =< V
aux(69) =< V-V1
s(88) =< aux(68)
s(117) =< aux(69)
s(15) =< aux(66)
s(12) =< aux(67)
s(38) =< aux(12)
aux(35) =< aux(38)
it(29) =< aux(38)
aux(35) =< aux(39)
it(29) =< aux(39)
aux(35) =< aux(68)
it(29) =< aux(68)
aux(37) =< aux(69)
s(90) =< it(29)*aux(69)
s(89) =< aux(35)
s(91) =< it(29)*aux(37)
with precondition: [V1>=2,Out>=2,V+3>=2*Out+2*V1]
* Chain [[29],30,40]: 6*it(29)+4*s(88)+1*s(89)+1*s(90)+1*s(91)+8*s(109)+3*s(110)+1*s(117)+11
Such that:aux(70) =< 1
aux(38) =< V/2
aux(39) =< V/2-V1/2
aux(71) =< V1
aux(72) =< V
aux(73) =< V-V1
s(88) =< aux(72)
s(117) =< aux(73)
s(110) =< aux(70)
s(109) =< aux(71)
aux(35) =< aux(38)
it(29) =< aux(38)
aux(35) =< aux(39)
it(29) =< aux(39)
aux(35) =< aux(72)
it(29) =< aux(72)
aux(37) =< aux(73)
s(90) =< it(29)*aux(73)
s(89) =< aux(35)
s(91) =< it(29)*aux(37)
with precondition: [V1>=2,Out>=2,V+3>=2*Out+2*V1]
* Chain [41]: 1*s(11)+11*s(12)+17*s(15)+3*s(22)+6*s(23)+1*s(26)+2*s(38)+5
Such that:s(26) =< -V+1
s(11) =< -V1+1
aux(9) =< 1
aux(10) =< -V+V1
aux(11) =< V
aux(12) =< V-V1
aux(13) =< V1
s(15) =< aux(9)
s(22) =< aux(10)
s(23) =< aux(11)
s(38) =< aux(12)
s(12) =< aux(13)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [40]: 4*s(109)+2*s(110)+5
Such that:aux(59) =< 1
aux(60) =< V1
s(110) =< aux(59)
s(109) =< aux(60)
with precondition: [V=0,Out=0,V1>=2]
* Chain [39]: 2*s(62)+4
Such that:aux(23) =< 1
s(62) =< aux(23)
with precondition: [V=1,V1=1,Out=0]
* Chain [38]: 2
with precondition: [V1=0,Out=0,V>=0]
* Chain [37]: 3
with precondition: [V1=0,Out=1,V>=0]
* Chain [36]: 4*s(93)+2*s(94)+5
Such that:aux(46) =< 1
aux(47) =< V1
s(94) =< aux(46)
s(93) =< aux(47)
with precondition: [Out=0,V1=V+1,V1>=2]
* Chain [35]: 2*s(99)+1*s(100)+4
Such that:s(100) =< 1
aux(49) =< V1
s(99) =< aux(49)
with precondition: [Out=0,V1=V,V1>=2]
* Chain [34,41]: 37*s(12)+11
Such that:aux(27) =< 1
s(12) =< aux(27)
with precondition: [V=1,V1=1,Out=1]
* Chain [33,41]: 36*s(12)+2*s(71)+1*s(73)+11
Such that:s(73) =< -V+1
aux(30) =< V
aux(32) =< 1
s(12) =< aux(32)
s(71) =< aux(30)
with precondition: [V1=1,Out=1,V>=2]
* Chain [31,41]: 1*s(11)+19*s(12)+19*s(15)+2*s(38)+11
Such that:aux(12) =< -V
s(11) =< -V+1
aux(53) =< 1
aux(54) =< V
s(15) =< aux(53)
s(12) =< aux(54)
s(38) =< aux(12)
with precondition: [Out=1,V=V1,V>=2]
* Chain [31,40]: 9*s(102)+3*s(103)+11
Such that:aux(61) =< 1
aux(62) =< V
s(103) =< aux(61)
s(102) =< aux(62)
with precondition: [Out=1,V=V1,V>=2]
* Chain [30,41]: 1*s(11)+18*s(12)+19*s(15)+2*s(38)+1*s(117)+1*s(119)+1*s(120)+11
Such that:s(119) =< -V+V1
s(120) =< V
s(117) =< V-V1
aux(12) =< -V1
s(11) =< -V1+1
aux(66) =< 1
aux(67) =< V1
s(15) =< aux(66)
s(12) =< aux(67)
s(38) =< aux(12)
with precondition: [Out=1,V1>=2,V>=V1+1]
* Chain [30,40]: 8*s(109)+3*s(110)+1*s(117)+1*s(119)+1*s(120)+11
Such that:s(119) =< -V+V1
s(120) =< V
s(117) =< V-V1
aux(70) =< 1
aux(71) =< V1
s(110) =< aux(70)
s(109) =< aux(71)
with precondition: [Out=1,V1>=2,V>=V1+1]
#### Cost of chains of plus(V,V1,Out):
* Chain [[43],44]: 1*it(43)+1
Such that:it(43) =< Out
with precondition: [V=0,Out>=1,V1>=Out]
* Chain [[42],[43],44]: 1*it(42)+1*it(43)+1
Such that:it(43) =< -V+Out
it(42) =< V
with precondition: [V>=1,Out>=V+1,V+V1>=Out]
* Chain [[42],44]: 1*it(42)+1
Such that:it(42) =< Out
with precondition: [V1>=0,Out>=1,V>=Out]
* Chain [44]: 1
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of start(V,V1,V15):
* Chain [56]: 8*s(306)+33*s(307)+18*s(308)+123*s(310)+1*s(327)+5*s(331)+105*s(334)+18*s(356)+3*s(358)+3*s(359)+3*s(360)+6*s(361)+2*s(362)+18*s(373)+3*s(375)+3*s(376)+3*s(377)+6*s(380)+1*s(381)+1*s(382)+1*s(383)+3*s(384)+11
Such that:s(327) =< -V+1
s(339) =< V-2*V1
s(363) =< V-V1+1
s(364) =< V/2-V1/2+1/2
aux(99) =< 1
aux(100) =< -V+V1
aux(101) =< V
aux(102) =< V-V1
aux(103) =< V/2
aux(104) =< V/2-V1/2
aux(105) =< -V1
aux(106) =< -V1+1
aux(107) =< V1
s(306) =< aux(100)
s(307) =< aux(101)
s(308) =< aux(102)
s(331) =< aux(106)
s(310) =< aux(107)
s(334) =< aux(99)
s(355) =< aux(103)
s(356) =< aux(103)
s(355) =< aux(104)
s(356) =< aux(104)
s(355) =< aux(101)
s(356) =< aux(101)
s(357) =< aux(102)
s(358) =< s(356)*aux(102)
s(359) =< s(355)
s(360) =< s(356)*s(357)
s(361) =< aux(105)
s(362) =< s(339)
s(372) =< aux(103)
s(373) =< aux(103)
s(372) =< aux(104)
s(373) =< aux(104)
s(375) =< s(373)*aux(102)
s(376) =< s(372)
s(377) =< s(373)*s(357)
s(379) =< aux(103)
s(380) =< aux(103)
s(379) =< aux(104)
s(380) =< aux(104)
s(379) =< s(364)
s(380) =< s(364)
s(381) =< s(380)*aux(102)
s(382) =< s(379)
s(383) =< s(380)*s(357)
s(384) =< s(363)
with precondition: [V>=0,V1>=0]
* Chain [55]: 2*s(402)+1
Such that:aux(108) =< V1
s(402) =< aux(108)
with precondition: [V=0,V1>=1]
* Chain [54]: 31*s(404)+62*s(406)+1*s(413)+2*s(418)+11
Such that:s(412) =< -V1
s(413) =< -V1+1
aux(109) =< 1
aux(110) =< V1
s(406) =< aux(109)
s(404) =< aux(110)
s(418) =< s(412)
with precondition: [V=V1,V>=1]
* Chain [53]: 1
with precondition: [V=1,V1>=0,V15>=0]
* Chain [52]: 5*s(419)+40*s(420)+382*s(425)+5*s(446)+68*s(490)+376*s(491)+14*s(500)+20*s(507)+30*s(523)+36*s(571)+6*s(573)+6*s(574)+6*s(575)+4*s(577)+36*s(592)+6*s(594)+6*s(595)+6*s(596)+12*s(599)+2*s(600)+2*s(601)+2*s(602)+6*s(603)+15
Such that:aux(152) =< 1
aux(153) =< -V1
aux(154) =< -V1+V15
aux(155) =< V1
aux(156) =< V1-3*V15
aux(157) =< V1-2*V15
aux(158) =< V1-2*V15+1
aux(159) =< V1-V15
aux(160) =< V1/2-V15
aux(161) =< V1/2-V15+1/2
aux(162) =< V1/2-V15/2
aux(163) =< -V15
aux(164) =< -V15+1
aux(165) =< V15
s(425) =< aux(152)
s(446) =< aux(153)
s(419) =< aux(154)
s(420) =< aux(155)
s(490) =< aux(159)
s(500) =< aux(164)
s(491) =< aux(165)
s(523) =< aux(157)
s(507) =< aux(163)
s(570) =< aux(162)
s(571) =< aux(162)
s(570) =< aux(160)
s(571) =< aux(160)
s(570) =< aux(159)
s(571) =< aux(159)
s(572) =< aux(157)
s(573) =< s(571)*aux(157)
s(574) =< s(570)
s(575) =< s(571)*s(572)
s(577) =< aux(156)
s(591) =< aux(162)
s(592) =< aux(162)
s(591) =< aux(160)
s(592) =< aux(160)
s(594) =< s(592)*aux(157)
s(595) =< s(591)
s(596) =< s(592)*s(572)
s(598) =< aux(162)
s(599) =< aux(162)
s(598) =< aux(160)
s(599) =< aux(160)
s(598) =< aux(161)
s(599) =< aux(161)
s(600) =< s(599)*aux(157)
s(601) =< s(598)
s(602) =< s(599)*s(572)
s(603) =< aux(158)
with precondition: [V=2,V1>=0,V15>=0]
* Chain [51]: 3
with precondition: [V=2,V1=0,V15=1]
* Chain [50]: 2*s(778)+3
Such that:aux(166) =< V15
s(778) =< aux(166)
with precondition: [V=2,V1=0,V15>=2]
* Chain [49]: 104*s(780)+372*s(781)+8*s(802)+8*s(803)+15
Such that:aux(179) =< 1
aux(180) =< V1
s(780) =< aux(180)
s(781) =< aux(179)
s(801) =< aux(180)-1
s(802) =< s(780)*aux(180)
s(803) =< s(780)*s(801)
with precondition: [V=2,V15=1,V1>=2]
* Chain [48]: 2*s(842)+3
Such that:aux(181) =< V15
s(842) =< aux(181)
with precondition: [V=2,V1+1=V15,V1>=1]
* Chain [47]: 23*s(844)+20*s(849)+1*s(853)+2*s(860)+9
Such that:aux(183) =< 1
s(852) =< -V15
s(853) =< -V15+1
aux(185) =< V15
s(844) =< aux(185)
s(849) =< aux(183)
s(860) =< s(852)
with precondition: [V=2,V1=V15,V1>=1]
* Chain [46]: 1*s(862)+139*s(865)+48*s(866)+4*s(868)+4*s(869)+11
Such that:s(862) =< -V+1
aux(186) =< 1
aux(187) =< V
s(865) =< aux(186)
s(866) =< aux(187)
s(867) =< aux(187)-1
s(868) =< s(866)*aux(187)
s(869) =< s(866)*s(867)
with precondition: [V1=1,V>=2]
* Chain [45]: 5*s(877)+2*s(880)+5
Such that:s(878) =< 1
aux(188) =< V1
s(877) =< aux(188)
s(880) =< s(878)
with precondition: [V+1=V1,V>=1]
Closed-form bounds of start(V,V1,V15):
-------------------------------------
* Chain [56] with precondition: [V>=0,V1>=0]
- Upper bound: 33*V+123*V1+116+nat(-V+V1)*8+nat(-V+1)+nat(-V1+1)*5+nat(V-V1+1)*3+nat(V-V1)*18+V/2* (nat(V-V1)*14)+nat(V-2*V1)*2+49/2*V
- Complexity: n^2
* Chain [55] with precondition: [V=0,V1>=1]
- Upper bound: 2*V1+1
- Complexity: n
* Chain [54] with precondition: [V=V1,V>=1]
- Upper bound: 31*V1+73
- Complexity: n
* Chain [53] with precondition: [V=1,V1>=0,V15>=0]
- Upper bound: 1
- Complexity: constant
* Chain [52] with precondition: [V=2,V1>=0,V15>=0]
- Upper bound: 40*V1+376*V15+397+nat(-V1+V15)*5+nat(-V15+1)*14+nat(V1-2*V15+1)*6+nat(V1-V15)*68+nat(V1-2*V15)*30+nat(V1-2*V15)*28*nat(V1/2-V15/2)+nat(V1-3*V15)*4+nat(V1/2-V15/2)*98
- Complexity: n^2
* Chain [51] with precondition: [V=2,V1=0,V15=1]
- Upper bound: 3
- Complexity: constant
* Chain [50] with precondition: [V=2,V1=0,V15>=2]
- Upper bound: 2*V15+3
- Complexity: n
* Chain [49] with precondition: [V=2,V15=1,V1>=2]
- Upper bound: 104*V1+387+8*V1*V1+ (8*V1-8)*V1
- Complexity: n^2
* Chain [48] with precondition: [V=2,V1+1=V15,V1>=1]
- Upper bound: 2*V15+3
- Complexity: n
* Chain [47] with precondition: [V=2,V1=V15,V1>=1]
- Upper bound: 23*V15+29
- Complexity: n
* Chain [46] with precondition: [V1=1,V>=2]
- Upper bound: 48*V+150+4*V*V+ (4*V-4)*V
- Complexity: n^2
* Chain [45] with precondition: [V+1=V1,V>=1]
- Upper bound: 5*V1+7
- Complexity: n
### Maximum cost of start(V,V1,V15): max([max([max([2,48*V+149+4*V*V+nat(V-1)*4*V]),nat(V15)*21+26+ (nat(V15)*2+2)]),9*V1+43+max([64*V1+max([8*V1*V1+271+nat(V1-1)*8*V1,33*V+19*V1+nat(-V+V1)*8+nat(-V+1)+nat(-V1+1)*5+nat(V-V1+1)*3+nat(V-V1)*18+V/2* (nat(V-V1)*14)+nat(V-2*V1)*2+49/2*V]),nat(V15)*376+281+nat(-V1+V15)*5+nat(-V15+1)*14+nat(V1-2*V15+1)*6+nat(V1-V15)*68+nat(V1-2*V15)*30+nat(V1-2*V15)*28*nat(V1/2-V15/2)+nat(V1-3*V15)*4+nat(V1/2-V15/2)*98])+ (26*V1+66)+ (3*V1+6)+2*V1])+1
Asymptotic class: n^2
* Total analysis performed in 1825 ms.